lens

lens

• definition
  • a lens
  • \[ \begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} B^{-} \\ B^{+} \end{pmatrix} \]
  • in a cartesian category \(\mathcal{C}\) consists of
    • a passforward map \(f: A^{+} \to B^{+}\)
      • sending information downstream
    • a passback map \(f^{\#}: A^{+} \times B^{-} \to A^{-}\)
      • sending information back upstream
      • it allows to use the value in \(A^{+}\), used by the downstreaming, to calculate how to pass information back upstream
• compose: lenses compose
  • given
    • \[ \begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} B^{-} \\ B^{+} \end{pmatrix} \]
    • \[ \begin{pmatrix} g^{\#} \\ g \end{pmatrix} : \begin{pmatrix} B^{-} \\ B^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} C^{-} \\ C^{+} \end{pmatrix} \]
    • we define their composite \(\begin{pmatrix}g^{\#} \\ g\end{pmatrix} \circ \begin{pmatrix}f^{\#} \\ f\end{pmatrix}\), with
      • passforward given by \(g \circ f\)
      • passback given by
        • \[ (a^{+}, c^{-}) \mapsto f^{\#}\left( a^{+}, g^{\#}(f(a^{+}), c^{-}) \right) \]
        • \[ (a^{+}, c^{-}) \mapsto \underbrace{ f^{\#}\left( a^{+}, \underbrace{ g^{\#}(\underbrace{ f(a^{+}) }_{ b^{+} }, c^{-}) }_{ b^{-} } \right) }_{ a^{-} } \]

category of lenses \(\mathbf{Lens}_{\mathbf{\mathcal{C}}}\)

• let \(\mathcal{C}\) be a cartesian category, then the category \(\mathbf{Lens}_{\mathbf{\mathcal{C}}}\) has:
• objects: pairs \(\begin{pmatrix}A^{-}\\A^{+}\end{pmatrix}\) of objects in \(\mathcal{C}\), called arenas
• morphisms: the lenses
  • \[ \begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} B^{-} \\ B^{+} \end{pmatrix} \]
• identity lens
  • \[ \begin{pmatrix} \pi_{2} \\ id \end{pmatrix} : \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \leftrightarrows \begin{pmatrix} A^{-} \\ A^{+} \end{pmatrix} \]
  • where \(\pi_{2}: A^{+} \times A^{-} \to A^{-}\) is the projection
• the composition is giving by lens composition
• it's named for its morphisms (lenses) rather than objects (arenas)
  • the category of charts, has arenas as objects but the morphisms are not lenses
  • double category \(\mathbf{Arena}^{\mathcal{C}}\), combining the category of lenses and category of charts, is named after its objects

Proposition: Functoriality of \(\mathbf{Lens}\)

• Every cartesian functor \(F: \mathcal{C} \to \mathcal{D}\) induces a functor \(\begin{pmatrix}F \\ F\end{pmatrix}: \mathbf{Lens_{\mathcal{C}}} \to \mathbf{Lens_{\mathcal{D}}}\), given by
  • \[ \begin{pmatrix} F \\ F \end{pmatrix} \begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} F f^{\#} \circ \mu^{-1} \\ F f \end{pmatrix} \]
  • where \(\mu = (F \pi_{1}, F \pi_{2}): F(X \times Y) \overset{ \sim }{ \to } FX \times FY\) is the isomorphism witnessing that \(F\) preserves products

Parallel product \(\otimes\)

• put two arenas in parallel
  • \(\begin{pmatrix}A_{1} \\ B_{1}\end{pmatrix}\) and \(\begin{pmatrix}A_{2} \\ B_{2}\end{pmatrix}\)
  • we just take their product in our cartesian category \(\mathcal{C}\)
  • \[ \begin{pmatrix}A_{1} \\ B_{1}\end{pmatrix} \otimes\begin{pmatrix}A_{2} \\ B_{2}\end{pmatrix} := \begin{pmatrix}A_{1} \times A_{2} \\ B_{1} \times B_{2} \end{pmatrix} \]
• parallel product for morphisms in \(\mathbf{Lens}\)
  • given
    • \[ \begin{pmatrix} f^{\#} \\ f \end{pmatrix} : \begin{pmatrix} A_{1} \\ B_{1} \end{pmatrix} \leftrightarrows \begin{pmatrix} C_{1} \\ D_{1} \end{pmatrix} \]
    • \[ \begin{pmatrix} g^{\#} \\ g \end{pmatrix} : \begin{pmatrix} A_{2} \\ B_{2} \end{pmatrix} \leftrightarrows \begin{pmatrix} C_{2} \\ D_{2} \end{pmatrix} \]
    • their parallel product is defined by
    • \[ \begin{pmatrix}f_{\#} \\ f\end{pmatrix} \otimes \begin{pmatrix}g_{\#} \\ g\end{pmatrix} := \begin{pmatrix}A_{1} \times A_{2} \\ B_{1} \times B_{2} \end{pmatrix} \leftrightarrows \begin{pmatrix}C_{1} \times C_{2} \\ D_{1} \times D_{2} \end{pmatrix} \]
  • it has
    • passforward \(f \times g\)
    • passback
      • \(((b_{1}, b_{2}), (c_{1}, c_{2})) \mapsto (f^{\#}(b_{1}, c_{1}), g^{\#}(b_{2}, c_{2}))\)
      • in terms of morphism, this is
      • \((B_1\times B_2)\times(C_1\times C_2)\overset{\sim}{\rightarrow}(B_1\times C_1)\times(B_2\times C_2)\overset{f^\#\times g^\#}{\longrightarrow}A_1\times A_2\)
  • together with \(\begin{pmatrix}1 \\ 1\end{pmatrix}\), this gives \(\mathbf{Lens}_{\mathcal{C}}\) the structure of a monoidal category
• Proposition
  • for cartesian functor \(F: \mathcal{C} \to \mathcal{D}\), the induced functor \(\begin{pmatrix}F \\ F\end{pmatrix}: \mathbf{Lens_{\mathcal{C}}} \to \mathbf{Lens_{\mathcal{D}}}\)
  • preserves the monidal product \(\otimes\), ie, it's strong monidal with respect to the parallel product
  • reference: 1.3.2.4 of Categorical System Theory

related

• cartesian category
• Categorical System Theory